Nuprl Lemma : w-M_wf
0,22
postcript
pdf
w
:World.
w
.M
IdLnk
Id
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
World
,
w
.M
,
t
T
Lemmas
world
wf
origin
w:World. w.M 
IdLnk
IdType w:World. w.M IdLnkIdType x:A. B(x) T